\section{Introduction}
In many languages, pattern matching can help making programs clear and concise.
Depending on the data structures one wants to work on, it can be the most
natural way to deal with execution control. Programs working on tree structures
or lists, for instance, can essentially be built almost exclusively using
pattern matching expressions. These in turn become large and complex, and the
process of checking their correctness cumbersome.

Interesting properties on pattern matching one may want to ensure
are \emph{completeness} and \emph{disjointness}, and sometimes both at the same
time, which is then refered to as \emph{partioning}.

A pattern matching expression is:
\begin{itemize}
\item \emph{complete} if for any value it can be tested against, at
\emph{least} one of its patterns will match it. Completeness is interesting for
obvious reasons; it guarantees that a program will behave as expected for all
possible values encountered.

\item It is \emph{disjoint} if for any value it can be tested against, at \emph{most}
one of its patterns will match it. Disjointness may be a less sought-after
property, however, when ensured, it gives a programmer confidence that its
pattern matching expression is well-written, in the sense that no pattern is
too ``tolerant'' and may thus cover cases which should be left to more precise
patterns. In languages where the first pattern which matches the selector is
executed, a nice property of disjoint matching expressions is that the patterns
can be reordered arbitrarily without changing the behaviour of the program.
\end{itemize}

These properties are in general not trivial to decide on, especially if the
patterns can be augmented with guards, that is, conditional expressions used to
refine them. There is only so much compilers can or are willing to do, and this
generally means that completeness is checked only very conservatively and
disjointness is not checked at all.

In this report we present techniques which can be used to generate formulae
representing completeness or disjointness for a given pattern matching
expression. Proving these formulae using a theorem prover is then equivalent to
declaring that the desired properties hold for that expression.

The following pages are organized as follows: first we will present the reader
with an overview of the Scala programming language, in particular the relevant
information about pattern matching. We will then cover the theoretical and
practical aspects underlying the generation of the formulae. We will conclude
with some notes on the status of our implementation and ideas regarding future
improvements.

